package tr.edu.ege.kipler.satisfiability.syntactical;

import java.util.Set;

import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.ConceptName;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class SHIQPreprocessingStrategy implements SyntacticalProcessingStrategy {
	private Reasoner reasoner;

	public SHIQPreprocessingStrategy(Reasoner reasoner) {
		this.reasoner = reasoner;
	}

	public WorldConstraintSystem process(Set<WorldElement> formulaSet) {
		WorldConstraintSystem result = reasoner.getProfile().getWcsFactory()
				.createWcs();
		World world = result.createWorld();
		for (WorldElement formula : formulaSet) {
			formula = formula.copy();
			FormulaSimplificationVisitor simpleVisitor = new FormulaSimplificationVisitor();
			formula.accept(simpleVisitor);
			formula = simpleVisitor.getNormalForm();
			world.addSilent(formula);
			addOldIndividualsToABox(world.getABox(), formula);
		}
		return result;
	}

	private void addOldIndividualsToABox(ABox abox, WorldElement formula) {
		IndividualCollectionFromFormulaVisitor visitor = new IndividualCollectionFromFormulaVisitor();
		formula.accept(visitor);
		try {
			for (String indv : visitor.getOldIndividualSet()) {
				abox.add(new ConceptAssertion(ConceptName.topConcept(), indv));
			}
		} catch (UnsatisfiableException e) {
			// will never reach here because none of the above assertions is
			// unsatisfiable
		}
	}

}
